Например, Бобцов

ПОДХОД К ВЕРИФИКАЦИИ АЛЛОКАТОРОВ ДИНАМИЧЕСКОЙ ПАМЯТИ, ОСНОВАННЫЙ НА СИМВОЛЬНОМ ВЫПОЛНЕНИИ ПРОГРАММ

Аннотация:

Предмет исследования. Исследованы техники эксплуатации уязвимостей в реализации алгоритмов распределения динамической памяти – аллокаторе библиотеки glibc (Poisoned Null-byte, Overlapped Chunks, Fastbin Attack, Unsafe Unlink, House of Einherjar, House of Force, House of Spirit, House of Lore, Unsorted Bin Attack). Приведены примеры кода эксплуатации уязвимостей и классификация представленных техник в соответствии с общим перечнем Common Weakness Enumeration. Исследованы современные методы и средства обнаружения уязвимостей, показаны их достоинства и недостатки на примере работы фреймворка Heap Hopper. Рассмотрены современные подходы к верификации программного обеспечения. Метод. Предложенный метод верификации программного обеспечения совмещает подходы статического анализа и символьного выполнения при использовании точной модели алгоритмов выделения динамической памяти. В процессе компиляции проверяемой программы создается структура Крипке. Уязвимости динамической памяти описываются формулами темпоральной логики. Полученная структура и формулы передаются на вход алгоритма проверки моделей. Осуществляется конкретно-символьное выполнение собранного бинарного файла. Для символьных путей выполнения проверяются условия уязвимостей, выраженные в виде формул пропозициональной логики. Основные результаты. Показана возможность практического применения предложенного подхода к обнаружению уязвимостей, возникающих при распределении динамической памяти в программных приложениях. Символьное выполнение реализовано в виде низкоуровневого отладчика, что позволяет снизить время работы алгоритмов за счет выполнения проверяемого приложения на реальном процессоре. Практическая значимость. Представлен комплексный подход для решения проблемы автоматического выявления уязвимостей на разных стадиях жизненного цикла разработки программного обеспечения. Предложенный подход применим для верификации аналогичных реализаций аллокаторов динамической памяти, таких как ptmalloc, dlmalloc, tcmalloc, jemalloc, musl.

Ключевые слова:

Постоянный URL

Статьи в номере

Содержание © 1993–2024 Университет ИТМО
Разработка © 2015 Университет ИТМО